$\forall$$A$:Dsys, $i$, $a$:Id. $a$ declared in M($i$) $\in$ Prop